The present invention relates generally to the field of microprocessors, and more particularly to the verification of integrated circuit designs.
Computational hardware designs are hierarchical in nature where modules within the hierarchy encapsulate a variety of logic functionality as a node. Logic designers and verification engineers tend to group together logical blocks that are functionally related into a functional (or logical) hierarchy for a circuit design. A functional hierarchy can then be transformed into a physical hierarchy that physically implements the functional hierarchy through integrated circuit components. For example, a functional hierarchy that calls for an “exclusive or” (XOR) gate can be transformed into a physical hierarchy containing a transistor circuit that physically produces a XOR result.
As a design for an integrated circuit evolves, formal equivalence checking is used to ensure that, while the internal structure of a design may change, the overall inputs and outputs of a functional hierarchy and physical hierarchy of a changed design remain unchanged (i.e., equivalent). Contrasting to equivalence checking, functional verification is the task of checking that a logical hierarchy conforms to what was intended. This may include functional verifications to any design changes to the logical hierarchy to ensure that, while the logical hierarchy may have changed, the outcome of the design change produces what was intended. Equivalence checking should not be confused with functional verification since equivalence checking confirms that both the functional hierarchy and the physical hierarchy both agree on an output for any randomly chosen input.
Logic synthesis is a process that converts a physical hierarchical high-level design, i.e., a hardware description language (HDL), such as a Very High Speed Integrated Circuit Hardware Description Language (VHSIC HDL, or more commonly known as VHDL) or Verilog, into a gate-level netlist. A netlist is a description of the connectivity of an electronic circuit, which can be comprised of a list of components in a circuit and a list of nodes they are connected to. A “gate-level” netlist is a design implementation description in terms of logic gates and interconnects, thus the gate-level netlist would comprise of a list of logic gates and a list of connections made between the logic gates. A synthesis tool is a computer program that performs logic synthesis in providing a gate-level netlist. Additionally, the gate-level netlist can be optimized for a variety of constraints while preserving the physical hierarchical high-level design. Such as optimizations for the gate-level netlist can accommodate for area, timing, and power constraints. These optimizations are verified to be correct by formal equivalence checking tools, which ensure the logic function, before and after the transformations/changes, are exactly the same. There are also a few optimizations that need to be verified by functional verification methods, which are often times unrelated to the core function of the logic, such as design-for-test logic (e.g., scan). In these cases, optimizations are back annotated into the logical hierarchical VHDL.
“Hierarchical references” are used to reflect the changes back to the logical VHDL without the need to rewrite and restructure substantial portions of the logic. Hierarchical references are a construct which allows making connections across design hierarchies which would otherwise not be feasible via port maps without reorganizing/rewiring the design, and adding or deleting components. A hierarchical reference denotes an object declared in a design hierarchy, and contains a path to the object being accessed. Individual elements in the path are separated by a dot (i.e., “.”). For example, a node in a functional hierarchy contains two hierarchical references named “rlm0.a” and “rlm0.b”. Another node in the functional hierarchy also has hierarchical references named “rlm1.c” and “rlm1.d”. The hierarchical references of the two macros can then be connected as such where rlm0.a feeds to rlm1.c (i.e., rlm1.c<=rlm0.a), and rlm1.c feeds to rlm0.b (i.e., rlm0.b<=rlm1.c). A hierarchy manipulation tool (e.g., Atrenta GenSys RTL) creates a physical hierarchy from a logical hierarchy, and can process hierarchical references and insert them at different levels of the logical hierarchy, to which the latter is transformed into a physical hierarchy.
“Blackboxing” lower level components enable a scalable hierarchical method to verify equivalence of design transformations, and is a common practice in functional and physical hierarchical design. Blackboxing is an abstraction which entails removing logic associated with a certain component or block, and replacing it with a shell having the same interface (input and output ports/pins). In a functional verification context, the outputs of the blackboxed component that serve as inputs for later logic are driven randomly, hence creating an over-approximation of prior logic in the logic sequence, which can then be used to prove correctness.
In an equivalence checking context, interface ports of blackboxed components across the two designs being equivalence checked are corresponded (i.e., if applicable, inputs to both blackboxes in a functional hierarchy and in a physical hierarchy are the same; and similarly, if applicable, outputs from both blackboxes in the functional hierarchy and in the physical hierarchy are the same). The input ports of the blackboxes can then be used to check for equivalence (i.e. miter'ed): randomly driving the output for both blackboxes generates the same input for both blackboxes. By virtue of this, the check ensures the values presented at the inputs of the corresponding blackboxes components are the same under all possible valuations of randomly driven inputs, making the overall equivalence check complete—in conjunction with other compare points such as design outputs, and correlating design inputs that are randomly driven.